Sections-16.agda:16,8-10
D !=< B.D of type Set
when checking that the expression !_ has type B.D
